Termination w.r.t. Q proof of TRS/SK904.38.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

g(f(x, y), z) → f(x, g(y, z))
g(h(x, y), z) → g(x, f(y, z))
g(x, h(y, z)) → h(g(x, y), z)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

g(f(x, y), z) → f(x, g(y, z))
g(h(x, y), z) → g(x, f(y, z))
g(x, h(y, z)) → h(g(x, y), z)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

G(h(x, y), z) → G(x, f(y, z))
G(f(x, y), z) → G(y, z)
G(x, h(y, z)) → G(x, y)

The TRS R consists of the following rules:

g(f(x, y), z) → f(x, g(y, z))
g(h(x, y), z) → g(x, f(y, z))
g(x, h(y, z)) → h(g(x, y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

G(h(x, y), z) → G(x, f(y, z))
G(f(x, y), z) → G(y, z)
G(x, h(y, z)) → G(x, y)

The TRS R consists of the following rules:

g(f(x, y), z) → f(x, g(y, z))
g(h(x, y), z) → g(x, f(y, z))
g(x, h(y, z)) → h(g(x, y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

G(h(x, y), z) → G(x, f(y, z))
G(f(x, y), z) → G(y, z)
G(x, h(y, z)) → G(x, y)

The TRS R consists of the following rules:

g(f(x, y), z) → f(x, g(y, z))
g(h(x, y), z) → g(x, f(y, z))
g(x, h(y, z)) → h(g(x, y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

G(x, h(y, z)) → G(x, y)

The remaining pairs can at least be oriented weakly.

G(h(x, y), z) → G(x, f(y, z))
G(f(x, y), z) → G(y, z)

Used ordering: Combined order from the following AFS and order.
G(x1, x2) = G(x2)
h(x1, x2) = h(x1, x2)
f(x1, x2) = f

Recursive path order with status [2].
Quasi-Precedence:

[G₁, h₂, f]

Status:

G₁: multiset
f: []
h₂: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

G(h(x, y), z) → G(x, f(y, z))
G(f(x, y), z) → G(y, z)

The TRS R consists of the following rules:

g(f(x, y), z) → f(x, g(y, z))
g(h(x, y), z) → g(x, f(y, z))
g(x, h(y, z)) → h(g(x, y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

G(h(x, y), z) → G(x, f(y, z))

The remaining pairs can at least be oriented weakly.

G(f(x, y), z) → G(y, z)

Used ordering: Combined order from the following AFS and order.
G(x1, x2) = G(x1, x2)
h(x1, x2) = h(x1, x2)
f(x1, x2) = x2

Recursive path order with status [2].
Quasi-Precedence:

[G₂, h_2]

Status:

G₂: multiset
h₂: [2,1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

G(f(x, y), z) → G(y, z)

The TRS R consists of the following rules:

g(f(x, y), z) → f(x, g(y, z))
g(h(x, y), z) → g(x, f(y, z))
g(x, h(y, z)) → h(g(x, y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

G(f(x, y), z) → G(y, z)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
G(x1, x2) = G(x1, x2)
f(x1, x2) = f(x1, x2)

Recursive path order with status [2].
Quasi-Precedence:

trivial

Status:

G₂: multiset
f₂: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

g(f(x, y), z) → f(x, g(y, z))
g(h(x, y), z) → g(x, f(y, z))
g(x, h(y, z)) → h(g(x, y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.